Rda(R)
== case R of 
== Rnone => 
== Rplus(left,right)=>rec1,rec2.
== Rinit(loc,T,x,v)=> 
== Rframe(loc,T,x,L)=> 
== Rsframe(lnk,tag,L)=> 
== Reffect(loc,ds,knd,T,x,f)=> knd : T
== Rsends(ds,knd,T,l,dt,g)=> knd : T  lnk-decl(l;dt)
== Rpre(loc,ds,a,T,P)=> locl(a) : T
== Raframe(loc,k,L)=> 
== Rbframe(loc,k,L)=> 
== Rrframe(loc,x,L)=>  

latex

---

clarification:

Rda(R)
== case R of 
== Rnone => 
== Rplus(left,right)=>rec1,rec2.
== Rinit(loc,T,x,v)=> 
== Rframe(loc,T,x,L)=> 
== Rsframe(lnk,tag,L)=> 
== Reffect(loc,ds,knd,T,x,f)=> knd : T
== Rsends(ds,knd,T,l,dt,g)=> fpf-join(KindDeq;knd : T;lnk-decl(l;dt))
== Rpre(loc,ds,a,T,P)=> locl(a) : T
== Raframe(loc,k,L)=> 
== Rbframe(loc,k,L)=> 
== Rrframe(loc,x,L)=>  

latex

Definitions	es realizer ind, f  g, KindDeq, lnk-decl(l;dt), x : v, locl(a),
FDL editor aliases	Rda